At a verification stage of a system development such as a software, from a formal model of a developed object system, a MBT (model-based testing) to automatically generate a test case (verification steps) to verify the system is used. As one of the MBT, from a state-transition system covering states and transitions possible for the system, a method for generating a test case by generating a path according to algorithm of graph theory is well known. By using the test case generated by this method, a test covering state transitions occurred in the system can be performed. Above method is disclosed in following references.                Non-patent reference 1 . . . Harold W. Thimbleby: “The directed Chinese Postman Problem”, In Software-Practice and Experience (SPE), Volume 33, pp. 1081-1096, 2003.        Non-patent reference 2 . . . Harold Abelson and Gerald Jay Sussman with Julie Sussman: “Structure and Interpretation of Computer Programs”, MIT Press, 1996.        
However, the state-transition system includes many similar state-transitions, and a test case acquired from the state-transition system is often redundant. For example, followings are examples of the test case in a task management function of an operating system.                Case 1: At a state “task 1 is waiting”, an event “wakeup (task 1)” occurs.        Case 2: At a state “task 2 is waiting”, an event “wakeup (task 2)” occurs.        
Difference between the cases 1 and 2 is only a task ID. It is sufficient that only one of the cases 1 and 2 is tested according to circumstances. Especially, in development of a large scale system, it is almost impossible that all cases are verified by covering. While coverage for items to be verified is maintained, it is realistic that all cases are suitably sampled and remained cases are tested.
As one solution, as disclosed in JP-A No. 2009-266092 (Kokai), following technique to generate a test case is proposed. Briefly, in this technique, a map for state sets of the state-transition system is given, and an equivalence relation between states is defined by equality of mapped values of the states by the map. Based on the equivalence relation, the state-transition system is previously contracted, and a test case is generated from the contracted state-transition system (quotient state-transition system).
Concretely, in this technique, states in the state-transition system are identified by an equivalence relation of mapped values by a state map indicated by a user. As to the equivalence relation of mapped values by the state map, states having equal output result (equal mapped values) by a state map are identified, and states having different output result (different mapped values) by the state map are not identified. In this case, the state map is a map from a state space.
Then, a plurality of states identified is grouped into one abstract state (one class), and the state-transition system can be small contracted. The abstract state is a virtual state which a plurality of states identified by the equivalence relation is recognized as one state. Furthermore, a test case can be generated to cover each state of the contracted (small) state-transition system at least one time.
FIGS. 3 and 4 are concrete examples by a task management function. In FIG. 3, a state map to output the number of tasks of each task state (RUN, RDY, WAI) is defined. When the number of tasks of each task is equal, these tasks are regarded as an equal state by not distinguishing each task ID. An example of the state-transition system contracted by this state map is shown in FIG. 4. In FIG. 4, the number of state-transition is contracted from 42 to 8.
In above-mentioned method, the state map largely influences a coverage and an efficiency (trade-off relation) of a test case to be output. However, as to a state map to generate the test case satisfying the coverage and the efficiency, there is not a means for reasonably determining the state map.